1. Field of the Invention
The present invention relates generally to hardware design verification, and in particular to verification of the design by extracting properties about the hardware design by analyzing the simulation data.
2. Description of the Related Art
The hardware designs of today are extremely complex and often include millions of transistors. One of the challenges with these extremely complex hardware designs is ensuring that the electrical circuits included in these hardware designs function as intended. Therefore, designers often use verification methods to confirm whether the design behavior conforms to the design purpose.
Traditional verification methods include simulation of the design. During simulation, millions of cycles of simulations are run for different sets of simulation vectors in order to determine whether the output would be as expected. However, verification methodology based on simulation is proving to be ineffective in finding deep corner-case design faults. Often, such design faults are found only after products implementing the design have been manufactured. This can lead to defective products, which in turn can result in millions of dollars in lost revenue.
Property checking (also sometimes referred to as model checking or formal verification) (PC) is another method another method used to test the circuit functionality. Generally in PC, a block of the design is taken at a time and it is determined whether for all possible inputs, a critical property is true. PC can be effective in finding corner-case design faults by exploring the design behavior on all possible input sequences. One of the obstacles with this approach is that the designer is required to specify a list of properties about the design to be proven through the PC method. The process is tedious and error prone. It is more than likely that the list of properties is not exhaustive and the likelihood of missing some of the required properties is high.
To solve this problem, there have been prior attempts to infer properties, either automatically, or based on directives already present in the design's source code. But, these properties have been based on either annotations already present in the design or properties, which are universal in designs. Examples of design properties which are universal are: a declared variable or net should not be constant, an array offset, should be within a declared range of the array, all states in a state machine should be reachable etc. Other previous efforts to ease the burden of writing properties include pre-packaged property annotations on library elements, thereby removing the need to specify particular properties everywhere that the library element is instantiated. Again, this requires manual property annotation for the library elements, along with the need to follow specific design/coding styles, and thus restricting the verification method to a simple class of checks such as “multiplexer select lines for a particular class of multiplexers should be one-hot”.
In view of the foregoing there is a need for a hardware design verification method that is effective in finding corner-case faults and also in inferring properties automatically.